package fos

import scala.util.parsing.combinator.syntactical.StandardTokenParsers
import scala.util.parsing.input._
import scala.util.parsing.syntax._
/** This object implements a parser and evaluator for the NB
 *  language of booleans and numbers found in Chapter 3 of
 *  the TAPL book.
 *  @author Jessa Bekker
 *  @author Nicolas Stucki
 */
object Arithmetic extends StandardTokenParsers {
  lexical.reserved ++= List("true", "false", "0", "if", "then", "else", "succ", "pred", "iszero")

  import lexical.NumericLit

  /** Expr ::= 'true'
      | 'false'
      | 'if' Expr 'then' Expr 'else' Expr
      | '0'
      | 'succ' Expr
      | 'pred' Expr
      | 'iszero' Expr
   */
  def Expr: Parser[Term] = (
       "if"~Expr~"then"~Expr~"else"~Expr  ^^ { case "if"~t1~"then"~t2~"else"~t3 => If(t1,t2,t3) }
     | "succ" ~> Expr ^^ { case nv:NumericalValue => SuccNV(nv); case t => Succ(t) }
     | "pred" ~> Expr ^^ { case t => Pred(t) }
     | "iszero" ~> Expr ^^ { case t => IsZero(t) }
     | "true" ^^ { case _ => True }
     | "false" ^^ { case _ => False }
     | "0" ^^ { case _ => Zero }
     | numericLit ^^ { case x => nvHelper(x.toInt) } // numerical literal
     | failure("illegal start of expression"))

  // Numerical literal decomposition
  private def nvHelper(n: Int): Term = if (n==0) Zero else SuccNV(nvHelper(n-1))

  def reduce(term: Term): Term = term match {
     case If(True,t2,_) => t2
     case If(False,_,t3) => t3
     case If(t1,t2,t3) => If(reduce(t1),t2,t3)
     case IsZero(Zero) => True
     case IsZero(Succ(_: NumericalValue)) => False
     case IsZero(t) => IsZero(reduce(t))
     case Pred(Zero) => Zero
     case Pred(Succ(nv: NumericalValue)) => nv
     case Pred(t) => Pred(reduce(t))
     case _ => term
  }
  
  def eval(term: Term): Term = term match {
     case  If(t1, t2, t3) => ( eval(t1), eval(t2), eval(t3) ) match { 
        case (True, v2: Value, _) 		=> v2  			// (B-IFTRUE)
        case (False, _, v3: Value) 	 	=> v3			// (B-IFFALSE)
        case (nv: NumericalValue, _, _) => term    		// Gets stuck
        case (stuckTerm, _, _) 		 	=> stuckTerm	// Throws back a stuck term
     }
     case Pred(t1) => eval(t1) match {
        case Zero 					  	=> Zero			// (B-PREDZERO)
        case Succ(nv: NumericalValue) 	=> nv			// (B-PREDSUCC)
        case False | True 			  	=> term			// Gets stuck
        case stuckTerm 				  	=> stuckTerm	// Throws back a stuck term
     }
     case Succ(t1) => eval(t1) match {			
        case _: Value  					=> term			// (B-SUCC) if it's a NumericalValue or gets stuck if it's True or False
        case stuckTerm 					=> stuckTerm	// Throws back a stuck term
     }
     case IsZero(t1) => eval(t1) match {
        case Zero 						=> True 		// (B-ISZEROZERO)
        case Succ(_: NumericalValue) 	=> False    	// (B-ISZEROSUCC)
        case True | False 				=> term			// Gets stuck
        case stuckTerm 					=> stuckTerm	// Throws back a stuck term
     }
     case v: Value 						=> v   			// (B-VALUE)
  }
     
  def main(args: Array[String]): Unit = {
   print("Input: ")
    val tokens = new lexical.Scanner(StreamReader(new java.io.InputStreamReader(System.in)))
    phrase(Expr)(tokens) match {
      case Success(tree, _) => {
	         def iterateReduceAndPrintSteps(term: Term): Term = {
	            println(term)
	            reduce(term) match {
	               case `term` 		=> term
	               case reducedTerm => iterateReduceAndPrintSteps(reducedTerm)
	            }
	         }
	         
	         println("Output:")
	         iterateReduceAndPrintSteps(tree) match {
	            case _: Value 	=> // OK, print nothing
	            case stuckTerm 	=> println("Stuck term: " + stuckTerm)
	         }
	         
	         eval(tree) match {
	            case v: Value 	=> println("Big step: " + v)
	            case stuckTerm 	=> println("Big step: Stuck term: " + stuckTerm)
	         }
         }
      case e => println(e)
    }
    
  }
}